es:ES, e:E. first(es-init(es;e)) ~ true 

latex

Definitions	x:A. B(x), t  T, es-init(es;e), true, Prop, P  Q, x. t(x), Y, if b t else f fi, false, SQType(T), {T}, , WellFnd{i}(A;x,y.R(x;y)), x(s), Unit, P  Q, P & Q, A, False,
Lemmas	bool sq, es-E wf, event system wf, es-locl-wellfnd, bool wf, es-first wf, es-init wf, btrue wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, es-pred wf, es-pred-locl, es-locl wf